package derivable;

import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
import java.util.Objects;
import java.util.Set;

/**
 * @author Henrik Wall
 * @author Rudolf Schmidt
 * @author Eugen Nemirowski
 */
public final class Conjunction implements Derivable<Conjunction>, Symbolized {
	private static final String SYMBOL = "&";

	private final Set<Proposition> propositions;

	private Conjunction(final Set<Proposition> propositions) {
		this.propositions = propositions;
	}

	/**
	 * Creates a new {@link Conjunction} of all the {@link Proposition}s.
	 * 
	 * @param propositions to be conjunct
	 * @return a new {@link Conjunction}
	 */
	public static Conjunction create(final Collection<? extends Proposition> propositions) {
		return new Conjunction(new HashSet<>(propositions));
	}

	/**
	 * Creates a new {@link Conjunction} of all the {@link Proposition}s.
	 * 
	 * @param propositions to be conjunct
	 * @return a new {@link Conjunction}
	 */
	public static Conjunction create(final Proposition... propositions) {
		final Set<Proposition> ps = new HashSet<>();
		Collections.addAll(ps, propositions);
		return new Conjunction(ps);
	}

	/**
	 * For {@link Conjunction}s c = {p<sub>1</sub>, …, p<sub>n</sub>} and c' =
	 * {p'<sub>1</sub>, …, p'<sub>m</sub>}: derives(c, c'): <=> For all j exists
	 * one i: derives(p<sub>i</sub>, p<sub>j</sub>')
	 */
	@Override
	public boolean derives(final Conjunction o) {
		j: for (final Proposition pj : o.propositions) {
			for (final Proposition pi : propositions) {
				if (pi.derives(pj))
					continue j;
			}
			return false;
		}
		return true;
	}

	@Override
	public String getSymbol() {
		return SYMBOL;
	}

	@Override
	public int hashCode() {
		final int prime = 31;
		int result = 1;
		result = prime * result + Objects.hashCode(propositions);
		return result;
	}

	@Override
	public boolean equals(Object obj) {
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (getClass() != obj.getClass())
			return false;
		final Conjunction other = (Conjunction) obj;
		return Objects.equals(propositions, other.propositions);
	}

	@Override
	public String toString() {
		if (propositions.isEmpty()) {
			return "()";
		}
		final StringBuilder sb = new StringBuilder("(");
		for (final Proposition proposition : propositions) {
			sb.append(proposition);
			sb.append(getSymbol());
		}
		sb.setLength(sb.length() - getSymbol().length());
		return sb.append(")").toString();
	}
}